T:Type, f:(TT), x:T. Dec(f(x) = x)  f(x) is f*(x) 

latex

Definitions

left + right, P  Q, Dec(P), y is f*(x), x:AB(x), x:A. B(x), Type, s = t, P  Q, t  T, y=f*(x) via L, <a, b>, , type List, f(a), , {i..j}, a < b, #$n, False, A, {x:A| B(x)} , n+m, l[i], A c B, P & Q, x:A  B(x), hd(l), i <z j, i z j, last(L), x:A. B(x), [], [car / cdr], Void, , tl(l), {T}, SQType(T), s ~ t, A  B, i  j < k, Atom, b, x,y:A//B(x;y), b | a, a ~ b, |p|, a  b, a <p b, |g|, a < b, x f y, |r|, xL. P(x), (xL.P(x)), Unit, ,

Lemmas

decidable int equal, guard wf, fun-path wf, int seg wf, not wf, false wf, decidable wf, fun-connected wf